Problem: f(f(X)) -> c(n__f(g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) d(X) -> n__d(X) activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X Proof: Bounds Processor: bound: 3 enrichment: match automaton: final states: {8,7,6,5,4} transitions: d1(65) -> 66* d1(10) -> 11* d1(71) -> 72* d1(63) -> 64* f1(55) -> 56* f1(57) -> 58* f1(49) -> 50* n__d1(35) -> 36* n__d1(29) -> 30* n__d1(26) -> 27* n__f1(45) -> 46* n__f1(37) -> 38* n__f1(43) -> 44* c1(27) -> 28* activate1(17) -> 18* activate1(19) -> 20* activate1(9) -> 10* n__d2(97) -> 98* n__d2(99) -> 100* n__d2(91) -> 92* n__d2(105) -> 106* n__f2(89) -> 90* n__f2(81) -> 82* n__f2(83) -> 84* d2(77) -> 78* d2(119) -> 120* d2(111) -> 112* d2(113) -> 114* f0(2) -> 4* f0(1) -> 4* f0(3) -> 4* activate2(76) -> 77* c0(2) -> 5* c0(1) -> 5* c0(3) -> 5* n__d3(107) -> 108* n__d3(131) -> 132* n__d3(123) -> 124* n__d3(125) -> 126* n__f0(2) -> 1* n__f0(1) -> 1* n__f0(3) -> 1* g0(2) -> 2* g0(1) -> 2* g0(3) -> 2* d0(2) -> 7* d0(1) -> 7* d0(3) -> 7* activate0(2) -> 8* activate0(1) -> 8* activate0(3) -> 8* h0(2) -> 6* h0(1) -> 6* h0(3) -> 6* n__d0(2) -> 3* n__d0(1) -> 3* n__d0(3) -> 3* 1 -> 8,65,55,43,29,17 2 -> 8,63,49,45,35,19 3 -> 8,71,57,37,26,9 9 -> 10* 10 -> 91* 11 -> 5* 17 -> 18,10 18 -> 10* 19 -> 20* 20 -> 10* 26 -> 119* 27 -> 76,7 28 -> 6* 29 -> 113* 30 -> 27* 35 -> 111* 36 -> 27* 38 -> 4* 44 -> 4* 46 -> 4* 49 -> 83* 50 -> 18,10,8 55 -> 89* 56 -> 18,10,8 57 -> 81* 58 -> 18,10,8 63 -> 99* 64 -> 10,8 65 -> 105* 66 -> 10,8 71 -> 97* 72 -> 10,8 76 -> 77* 77 -> 107* 78 -> 28,6 82 -> 58* 84 -> 50,8 90 -> 56,8 92 -> 11* 98 -> 72* 100 -> 64,8 106 -> 66,8 108 -> 78,28 111 -> 123* 112 -> 77* 113 -> 125* 114 -> 77* 119 -> 131* 120 -> 77* 124 -> 112* 126 -> 114,77,107 132 -> 120,77,107 problem: Qed